Termination of the following Term Rewriting System could be proven:

Context-sensitive rewrite system:
The TRS R consists of the following rules:

terms(N) → cons(recip(sqr(N)), terms(s(N)))
sqr(0) → 0
sqr(s(X)) → s(add(sqr(X), dbl(X)))
dbl(0) → 0
dbl(s(X)) → s(s(dbl(X)))
add(0, X) → X
add(s(X), Y) → s(add(X, Y))
first(0, X) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))

The replacement map contains the following entries:

terms: {1}
cons: {1}
recip: {1}
sqr: {1}
s: empty set
0: empty set
add: {1, 2}
dbl: {1}
first: {1, 2}
nil: empty set


↳ CSR
  ↳ CSRInnermostProof

Context-sensitive rewrite system:
The TRS R consists of the following rules:

terms(N) → cons(recip(sqr(N)), terms(s(N)))
sqr(0) → 0
sqr(s(X)) → s(add(sqr(X), dbl(X)))
dbl(0) → 0
dbl(s(X)) → s(s(dbl(X)))
add(0, X) → X
add(s(X), Y) → s(add(X, Y))
first(0, X) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))

The replacement map contains the following entries:

terms: {1}
cons: {1}
recip: {1}
sqr: {1}
s: empty set
0: empty set
add: {1, 2}
dbl: {1}
first: {1, 2}
nil: empty set

The CSR is orthogonal. By [10] we can switch to innermost.

↳ CSR
  ↳ CSRInnermostProof
    ↳ CSR
      ↳ CSDependencyPairsProof

Context-sensitive rewrite system:
The TRS R consists of the following rules:

terms(N) → cons(recip(sqr(N)), terms(s(N)))
sqr(0) → 0
sqr(s(X)) → s(add(sqr(X), dbl(X)))
dbl(0) → 0
dbl(s(X)) → s(s(dbl(X)))
add(0, X) → X
add(s(X), Y) → s(add(X, Y))
first(0, X) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))

The replacement map contains the following entries:

terms: {1}
cons: {1}
recip: {1}
sqr: {1}
s: empty set
0: empty set
add: {1, 2}
dbl: {1}
first: {1, 2}
nil: empty set

Innermost Strategy.

Using Improved CS-DPs we result in the following initial Q-CSDP problem.

↳ CSR
  ↳ CSRInnermostProof
    ↳ CSR
      ↳ CSDependencyPairsProof
        ↳ QCSDP
          ↳ QCSDependencyGraphProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {terms, recip, sqr, add, dbl, first, SQR, TERMS, ADD, DBL, FIRST} are replacing on all positions.
For all symbols f in {cons} we have µ(f) = {1}.
The symbols in {s, U} are not replacing on any position.

The ordinary context-sensitive dependency pairs DPo are:

TERMS(N) → SQR(N)


The hidden terms of R are:

terms(s(N))
add(sqr(X), dbl(X))
sqr(X)
dbl(X)
add(X, Y)
first(X, Z)

Every hiding context is built from:

sqr on positions {1}
dbl on positions {1}
add on positions {1, 2}
first on positions {1, 2}

Hence, the new unhiding pairs DPu are :

U(sqr(x_0)) → U(x_0)
U(dbl(x_0)) → U(x_0)
U(add(x_0, x_1)) → U(x_0)
U(add(x_0, x_1)) → U(x_1)
U(first(x_0, x_1)) → U(x_0)
U(first(x_0, x_1)) → U(x_1)
U(terms(s(N))) → TERMS(s(N))
U(add(sqr(X), dbl(X))) → ADD(sqr(X), dbl(X))
U(sqr(X)) → SQR(X)
U(dbl(X)) → DBL(X)
U(add(X, Y)) → ADD(X, Y)
U(first(X, Z)) → FIRST(X, Z)

The TRS R consists of the following rules:

terms(N) → cons(recip(sqr(N)), terms(s(N)))
sqr(0) → 0
sqr(s(X)) → s(add(sqr(X), dbl(X)))
dbl(0) → 0
dbl(s(X)) → s(s(dbl(X)))
add(0, X) → X
add(s(X), Y) → s(add(X, Y))
first(0, X) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))

The set Q consists of the following terms:

terms(x0)
sqr(0)
sqr(s(x0))
dbl(0)
dbl(s(x0))
add(0, x0)
add(s(x0), x1)
first(0, x0)
first(s(x0), cons(x1, x2))


The approximation of the Context-Sensitive Dependency Graph contains 1 SCC with 7 less nodes.


↳ CSR
  ↳ CSRInnermostProof
    ↳ CSR
      ↳ CSDependencyPairsProof
        ↳ QCSDP
          ↳ QCSDependencyGraphProof
            ↳ QCSDP
              ↳ QCSDPSubtermProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {terms, recip, sqr, add, dbl, first} are replacing on all positions.
For all symbols f in {cons} we have µ(f) = {1}.
The symbols in {s, U} are not replacing on any position.

The TRS P consists of the following rules:

U(sqr(x_0)) → U(x_0)
U(dbl(x_0)) → U(x_0)
U(add(x_0, x_1)) → U(x_0)
U(add(x_0, x_1)) → U(x_1)
U(first(x_0, x_1)) → U(x_0)
U(first(x_0, x_1)) → U(x_1)

The TRS R consists of the following rules:

terms(N) → cons(recip(sqr(N)), terms(s(N)))
sqr(0) → 0
sqr(s(X)) → s(add(sqr(X), dbl(X)))
dbl(0) → 0
dbl(s(X)) → s(s(dbl(X)))
add(0, X) → X
add(s(X), Y) → s(add(X, Y))
first(0, X) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))

The set Q consists of the following terms:

terms(x0)
sqr(0)
sqr(s(x0))
dbl(0)
dbl(s(x0))
add(0, x0)
add(s(x0), x1)
first(0, x0)
first(s(x0), cons(x1, x2))


We use the subterm processor [20].


The following pairs can be oriented strictly and are deleted.


U(sqr(x_0)) → U(x_0)
U(dbl(x_0)) → U(x_0)
U(add(x_0, x_1)) → U(x_0)
U(add(x_0, x_1)) → U(x_1)
U(first(x_0, x_1)) → U(x_0)
U(first(x_0, x_1)) → U(x_1)
The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
U(x1)  =  x1

Subterm Order


↳ CSR
  ↳ CSRInnermostProof
    ↳ CSR
      ↳ CSDependencyPairsProof
        ↳ QCSDP
          ↳ QCSDependencyGraphProof
            ↳ QCSDP
              ↳ QCSDPSubtermProof
                ↳ QCSDP
                  ↳ PIsEmptyProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {terms, recip, sqr, add, dbl, first} are replacing on all positions.
For all symbols f in {cons} we have µ(f) = {1}.
The symbols in {s} are not replacing on any position.

The TRS P consists of the following rules:
none

The TRS R consists of the following rules:

terms(N) → cons(recip(sqr(N)), terms(s(N)))
sqr(0) → 0
sqr(s(X)) → s(add(sqr(X), dbl(X)))
dbl(0) → 0
dbl(s(X)) → s(s(dbl(X)))
add(0, X) → X
add(s(X), Y) → s(add(X, Y))
first(0, X) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))

The set Q consists of the following terms:

terms(x0)
sqr(0)
sqr(s(x0))
dbl(0)
dbl(s(x0))
add(0, x0)
add(s(x0), x1)
first(0, x0)
first(s(x0), cons(x1, x2))


The TRS P is empty. Hence, there is no (P,Q,R,µ)-chain.